The Formal System of Dijkstra and Scholten

Rocha, Camilo | 2015

The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding this logic to the point in which, for some time, it was not considered a logic, as logicians use the word. The main objections arise from the fact that: (i) symbolic manipulations seem to be based on the meaning of the terms involved, and (ii) some notation and the proof style of the logic are different, to some extent, from those found in the traditional use of logic. This paper presents the Dijkstra-Scholten logic as a formal system, and explains its proof-theoretic foundations as a formal system, thus avoiding any confusion regarding term manipulation, notation, and proof style. The formal system is shown to be sound and complete, mainly, by using rewriting and narrowing based decision and semi-decision procedures for, respectively, propositional and first-order logic previously developed by C. Rocha and J. Meseguer.